package ch.epfl.lara.matcheck.verify;

import ch.epfl.lara.matcheck.ast.{Formula,Imply,And,Or,Neg,Tru,Flse}

abstract class VerifyMatch extends MatchProperties {
  
  
  override protected def disjoint(axiom: Axiom, patterns: List[Imply]): Formula = {
    var rhs: Formula = Tru 
    for(i<-List.range(0,patterns.length); j<-List.range(i+1,patterns.length)) {
      val Imply(i_lhs,i_rhs) = patterns(i)
      val Imply(j_lhs,j_rhs) = patterns(j)
      rhs = And(rhs,Imply(And(i_lhs,j_lhs),Neg(And(i_rhs,j_rhs))))
    }
    Imply(axiom,rhs)
  }
  

  
  
  override protected def complete(axiom: Axiom, patterns: List[Imply]): Formula = 
    patterns match {
      case Nil          => Imply(axiom,Tru)
      case head :: tail => Imply(axiom,tail.foldLeft[Formula](head)((acc,e) => Or(acc,e)))
    }
  
  
  
  
  override protected def unreachable(axiom: Axiom, patterns: List[Imply]): List[Formula] =  {
    var acc: Formula = Tru
    for(x @ Imply(lhs,rhs)<-patterns) yield {
      acc = And(acc,lhs)
      val formula = Imply(And(axiom,acc),Neg(rhs))
      acc = And(acc,Neg(rhs))
      formula
    }
  }
}
